\documentclass[a4paper,10pt]{article}

\usepackage{amsfonts, amsmath, amsthm, amssymb}
\usepackage[english]{babel}
%\usepackage{bookman}
%\usepackage{pxfonts}

%\usepackage[T1]{fontenc}
\usepackage{subfig}
\usepackage{graphicx}
\usepackage{lmodern}
\usepackage[utf8]{inputenc}
\usepackage{a4wide}
\usepackage{hyperref}
\pagestyle{headings}
\pagestyle{plain}
\usepackage{url}

\newcommand{\true}{\mathsf{true}}
\newcommand{\false}{\mathsf{false}}

\newcommand{\mint}[1]{\;\mathrm{#1}}
\newcommand{\then}{\Rightarrow}

\newcommand{\w}{\mathbf{w}}
\renewcommand{\c}{\mathbf{c}}
\newcommand{\1}{\mathbf{1}}


%\frenchspacing

\title{Automatic reasoning, assignment 3 \\ Eleven Stones}
\author{Niklas Weber \\ 0841420, \\ Matúš Tejiščák \\ 4176200}
\date{\today}

\begin{document}

\maketitle

\section{The problem}
The question is: In how many ways can eleven stones be placed on a $11*11$ field, while being subject to certain constraints (see below)?

\section{Representation of the game model}
The question given suggests an implementation as a bddsolve problem. As such, we shall look for a model given only in first-order propositional (boolean) logic.

The board is represented by a $m*n$-matrix of boolean variables\footnote{Note, that this is a generalization of the original problem, which expressively states a $11*11$-matrix.}. $v\_a\_b$ means: there is a stone placed at point $(a,b)$\footnote{With $1 \leq a \leq m \text{ and } 1 \leq b \leq n$}.

We see, that there are three basic types of constraints.
\begin{enumerate}
\item Reserved positions: \\
$(2, y) \text{ for } y \leq 5$\\
$(x, 4) \text{ for } 4 \leq x \leq 8$\\
$(10, y) \text{ for } 4 \leq y \leq 11$\\
$(x, y) \text{ for } 2 \leq x \leq 8 \text{ and } 7 \leq y \leq 8$\\

\item Mutual exclusive positions:\\
Only one stone per row\\
Only one stone per column\\
Distance between each stone $> \sqrt{6}$

\item 11 stones are being placed
\end{enumerate}
Let us begin by inspecting the first type of constraint: reserved fields.\\
Let $R$ be the set of tuples $(a,b)$ for which holds: the position denoted by the tuple lies inside the field's boundaries and at least one of the 'reserved position' constraints is violated.
Then we can express the union of these constraints as:
\begin{align}
	\bigwedge_{(a,b) \in R} & \neg v\_a\_b
		& \text{(Reserved positions are unoccupied)}
\end{align}
Next we shall focus on the constraints of mutual exclusiveness. Effectively they can be translated as 'if there is a stone on $(a,b)$ then there must be no stone on $(a',b')$ because of the \{row/column/distance\} constraint'. If one has seen this, the three conditions can be encoded in a straightforward manner:
\begin{align}
	\bigwedge_{a,b}  ( v\_a\_b & \Longrightarrow 
	\bigwedge_{a' \neq a} \neg v\_a'\_b)
		& \text{(No two stones in one column)}
\end{align}
\begin{align}
	\bigwedge_{a,b}  ( v\_a\_b & \Longrightarrow 
	\bigwedge_{b' \neq b} \neg v\_a\_b')
		& \text{(No two stones in one row)}
\end{align}
\begin{align}
	\bigwedge_{a,b}  (v\_a\_b & \Longrightarrow 
	\bigwedge_{(a',b') \neq (a,b) \text{ and } (a-a')^2 + (b-b')^2 >  6
} \neg v\_a\_b')
		& \text{(Distance between each stone } > \sqrt{6} \text{)}
\end{align}
Of course these implications can be conflated into one by making a conjunction of all the consequents (i. e. illegal fields) belonging to one antecedent (i.e. field where the stone is placed).

A reduction in size can be achieved, if the reserved positions are left out. This is possible in two senses: First, should there be such a position in the antecedent all of the rules having this antecedent may be omitted (as then the antecedent is always false and the implication as a whole always true). Regarding the formalization above this would mean that, for example, a complete rule $(a,b) \Longrightarrow \neg (a',b') \wedge \neg (a'',b'') \wedge ...$ may be removed if $(a,b)$ is reserved.

Second, should there be such a position in the consequent this specific conjunct may be omitted (as then the consequent is always true, as is the implication as a whole). An example: if $(a,b) \Longrightarrow \neg (a',b') \wedge \neg (a'',b'') \wedge ...$ and we know that $(a',b')$ is reserved we can shorten the rule to $(a,b) \Longrightarrow \wedge \neg (a'',b'') \wedge ...$.\\
This also makes sense intuitively: rules of mutual exclusiveness add no information if at least one of the two positions involved is always empty.

The final formula, which is tested for satisfiability is formed by combining the formulae for reserved positions and mutual exclusiveness through conjunction.

The last constraint, that there are eleven stones to be placed, is rather unhandy when written out in a generalized way. The best we can concoct is to give a disjunction of every 11-tuple of (different) fields not containing reserved places. If, instead, we accept the premiss that we are, \textit{in concreto}, dealing with a $11*11$ field here and if we furthermore take the 1-per-column / 1-per-row constraints into account we can formulate a much simpler requirement:
\begin{align}
\bigwedge_{1 \leq a \leq 11} (\bigvee_{1 \leq b \leq 11} & v\_a\_b) & \text{(At least one stone is placed in every row)}
\end{align}
As now we have at least one stone per row and, by merit of the constraints, at most one stone per row we can be certain that the resulting valuation has exactly one stone for every row, which equals 11 stones.

This formalization forms the basis of our own implementation, as described below. 

\paragraph{Alternative formalization:} The crucial point is, that all of the constraints of mutual exclusiveness are symmetric. We can formalize this as:\\ $(a,b) \Rightarrow \neg (a',b') \Leftrightarrow (a',b') \Rightarrow \neg (a,b)$\\
Intuitively this makes sense, 'being in the same row as', 'being in the same column as' and 'having a distance $\leq \sqrt{6}$ to' are symmetric relations. This means, that we can construct a set of (unordered) pairs of positions. Every of these pairs describes two positions which may not be occupied simultaneously. Let $ME$ be this set. Then
\begin{align}
	\bigwedge_{((a,b), (a',b')) \in ME}  & \neg (v\_a\_b \wedge v\_a'\_b')  & 
			& \text{(No mutual exclusive pair)}
\end{align}
Again, pairs containing reserved positions can be filtered out (as then the negated conjunction would always be true).
We do think that this forms a minimal formalization. A second implementation based on this model has been developed, but time has been too limited to debug it properly.
\section{Implementation}
As indicated, this refers to the non-minimal model.
When looking at the formulae described above one may notice that non-standard expressions have only been used in the meta language used to describe big conjunctions. More precisely: they are only used for the ranges ($(a,b) \in R$ etc.). When one unfolds these expression the result is an ordinary first-order propositional logic formula.

This unfolding has been implemented by means of a Python script\footnote{\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/task3.py}}. We assume that a description of the Python code is outside of the focus of this document.
\section{Solution}
We have employed BDDSolve's \textsc{SAT} logic, applied to the formula generated by the Python script mentionend above. The variables are ordered lexicographically. This is a satisfying assignment found by Yices:
\setcounter{MaxMatrixCols}{20}
\begin{figure}[htp]
	\begin{center}
	\include{task3-appendix-1}
	\end{center}
	
	\caption{A solution to the problem found by BDDSolve\\
	Legend: $\bullet$ = stone, $\cdot$ = not occupied, $-$ = reserved, ! = conflict (does not occur)}
	\label{fig:sol-1}
\end{figure}

\end{document}




























